


We have proposed the concept of \emph{adaptable process} 
as a way of describing complex evolvability patterns 
in models of concurrent systems.
We have introduced \evol{}, a process calculus of adaptable processes, in which located processes can be updated and relocated at runtime. 
This ability goes beyond the kind of reconfiguration possible in existing process calculi. 
In the design of \evol{}, we aimed at isolating the minimal basis for representing 
reconfiguration of interacting processes:
we extended CCS without restriction and relabeling (a non Turing complete model), 
with transparent localities (arguably the simplest conceivable way of structuring processes into hierarchies) 
and with update prefixes. 
The interaction of adaptable processes with update prefixes constitutes 
a minimal form of higher-order communication that realizes process reconfiguration.

In order to formalize the correctness of evolvable processes, we have proposed %two verification problems:
the \emph{bounded} and \emph{eventual} adaptation problems.
We have studied the (un)decidability  
of these two problems in several variants of \evol{}, obtained by 
different evolvability patterns as well as static and dynamic topologies of adaptable processes.
Our results shed light on the expressive power of  \evol{} as well as on the 
nature of verification for 
concurrent processes that may evolve at runtime.

There are a number of issues associated to adaptable processes that would be worth investigating  in future work.
It would be interesting to study  the behavioral theory of \evol{} processes;
recent works on behavioral equivalences for higher-order process calculi with passivation (e.g. \cite{LengletSS11,PierardS11}) 
could provide a reasonable starting point.
From a practical standpoint, 
it would be interesting to 
develop extensions or variants of \evol{} tailored to concrete application settings,
to determine how 
the adaptation problems 
proposed here fit in such scenarios, and to study how to transfer our decidability results to such richer languages.
Closely related, it would be useful to address also 
the complexity of \OG and \LG.
%While considering concrete applications, it would also be interesting to assess the problem of complexity.
%As far as we know, the decidability of \OG could be very demanding. Decidability is guaranteed by the fact that our LTS (for \evold{2}) is a well-structured transition system, this ensure the termination of the procedure but it does not say anything on the actual complexity.
As far as \LG is concerned, we have presented its (polynomial) 
reduction to the Petri net place boundedness problem,
for which an EXPSPACE decision procedure exists \cite{Rackoff78}.
Concerning \OG, our proof of decidability does not give a precise indication
about the complexity, as only the termination of the procedure
is guaranteed by the well quasi-ordering we have defined.
We plan to investigate the complexity of the problem 
by comparing \OG to the coverability problem for reset Petri nets
which is known to be non primitive recursive
(see, e.g., \cite{Schnoebelen10}). 
In fact, the possibility of atomically erasing the current contents of an adaptable
process is reminiscent of the ability that reset transitions have for removing
all the tokens in some given place.
Hence, a plausible direction of future work is to 
investigate suitable abstractions  that could help alleviating 
the state explosion problem.


%Rackoff, C.: The covering and boundedness problems for vector addition systems.
%Theoret. Comp. Sci. 6, 223Ð231 (1978)
%Schnoebelen, P.: Revisiting Ackermann-Hardness for Lossy Counter Machines and Reset Petri Nets. In: Hlin?n?, P., Ku?era, A. (eds.) MFCS 2010. LNCS, vol. 6281,
%pp. 616Ð628. Springer, Heidelberg (2010)

%\todo{\bf VAL LA PENA DIRE CHE LASCIAMO LO STUDIO DELLA COMPLESSITA'
%DEL PROBLEMA PER LAVORI FUTURI. POSSIAMO DIRE CHE PER LE RETI DI
%PETRI, LA NOSTRA DIMOSTRAZIONE DI DECIDIBILITA' SI RIDUCE
%ALLA COVERABILITY CHE HA GIA' COMPLESSITA' 2EXPSpace (CINZIA, NON HO
%SOTTO I PAPER QUINDI CONTROLLA CHE NON ABBIA DETTO UNA CAGATA),
%MENTRE LA TECNICA CHE SI RIFA AI WSTS CI PERMETTE DI DIMOSTRARE
%LA TERMINAZIONE DELLA PROCEDURA --GRAZIE AL WQO-- SENZA DARE PERO'
%PRECISE INDICAZIONI DELLA COMPLESSITA', CHE PERO' POTREBBE
%RICHIEDERE NOTEVOLE COMPLESSITA' (VEDI AD ESEMPIO COVERABILITY
%IN PETRI NET CON RESET CHE QUESTA TECNICA PERMETTE DI VERIFICARE
%MA CHE SI SA ESSERE PROBLEMA NON PRIMITIVO RICORSIVO --VEDI UN PAPER DI 
%SCHNOEBELEN DELLO SCORSO ANNO O POCO PRIMA).
%QUINDI POTREBBE ESSERE UTILE IN FUTURO SVILUPPARE TECNICHE
%ASTRATTE PIU' EFFICIENTI CHE POTREBBERO ESSERE STUDIATE (E QUESTE
%POTREBBERO ESSERE POI APPLICATE A LINGUAGGI "REALI")}


%
% OLD VERSION 
% 
%We have 
%provided 
%a complete investigation of  the (un)decidability properties of 
%\emph{bounded} and \emph{eventual} adaptation, 
%two novel correctness properties for component-based systems.
%%two correctness properties of \emph{aggregations} of components.
%Our study has relied on the \evol{} calculus, 
%an extension of Milner's CCS with a construct for components
%and update capabilities.
%The (un)decidability of the adaptation properties is 
%analyzed in different varants of \evol{} which 
%result from considering dynamic and static component topologies 
%as well as 
%three different possibilities for behavior associated to update capabilities.
%Our results shed light on the nature of verification in a number of application 
%areas in which software construction proceeds by the systematic combination
%of predefined blocks. 
%%Although along the paper we have made reference to the use of our approach
%%to the case of cloud computing scenarios (in which the building blocks are web services), 
%%we do not make assumptions on a particular application context; 
%%rather, 
%%we believe that our results 
%%are general enough so as to 
%%have a place also
%%in languages for service-oriented computing and workflow management/business processes.
%As discussed in the introduction, we plan to  
%investigate the influence behavioral interfaces have on 
%the expressiveness of process calculi for components and on the 
%(un)decidability of associated correctness properties.
%In this spirit, investigating whether the constructs 
%of (fragments of) \evol{} can be suitable enriched with the kind of interfaces defined 
%in MECo \cite{MontesiS10} appears interesting.
%
%% on the 
%%expressiveness and decidability %properties
%%%calculi: \comp{0}, \comp{1} and \comp{2} to identify 
%%of six process calculi for component-based systems.
%
%%DISCUSS/SUMMARIZE RESULTS HERE
%%determine a hierarchy of calculi of increasing expressiveness. 
%% \comp{0} is a basic language 
%% without constructs for update,
%% in which transparent localities represent components.
%% Termination properties for \comp{0} are decidable. %is analogous to the one of Petri nets. 
%% \comp{1} extends \comp{0} with \emph{static update}. 
%% In \comp{1}, %in \comp{1} 
%% termination 
%% for \comp{1} processes
%% is decidable, as is the model-checking problem for a simple spatial logic. 
%% This way, interesting properties (most notably, safety ones) can be effectively checked.
%% However, convergence is undecidable so the language is not trivial.
%% %, and hence it is more expressive than \comp{0}. 
%% Finally, 
%% \comp{2} is a higher-order extension of \comp{1} with a \emph{dynamic update} construct.
%% \comp{2} is Turing complete: hence, most interesting decision problems are undecidable.
%% The different mechanisms for update (including its absence) 
%% thus induce a hierarchy of languages of increasing expressive power.
%
%%We studied 
%%very simple process calculi 
%%with update constructs 
%%as our main interest was in 
%%identifying the sources of expressiveness of these languages.
%
%
%%proposed here. Here we rely on decidability of properties that follows from the ability of providing a well quasi order on the LTS. In \cite{BliudzeS08} they use the ability of mimic rules of both languages (Glues) which needs to put some strong restriction on how the Glue is mimicked.
%
%%\todo{M-calculus? Seal? altri?}
%% Plans for future work include assessing the robustness of the results
%% presented here. An initial direction is to consider the variant of \comp{1}
%% with recursive definitions instead of replication. 
%% We conjecture that it is still possible to obtain a well-structured transition
%% system for such a variant (and hence to show that termination is decidable) but the details
%% of the proofs become much more involved. 
%% Another direction is to 
%% consider variants of transparent localities with different ``opacity'' properties
%% and to study their relationship with the expressiveness of update mechanisms. 
%
%% Much work remains to be done on understanding the expressive power of operators like the one of passivation. We plan to extend this work along two lines: on one side following the idea in \cite{Busi} we should consider what happens in presence of a dofferent source of infinite behaviour as with recursion. Our guess is that there is no gap between the languages. The other line instead focuses more on the power of the operator of passivation and by changing its capabilities: i.e. what kind of messages can be sent along the same ideas in \cite{GiustoPZ09} or by changing the transparency/opacity of the operator.
%
%% 
%% In \cite{BliudzeS08} it has been proved that BIP is more expressive than CCS, more precisely the authors provide a framework for comparing expressiveness of calculi. Nevertheless the tecniques adoptedthere are different from the ones proposed here. Here we rely on decidability of properties that follows from the ability of providing a well quasi order on the LTS. In \cite{BliudzeS08} they use the ability of mimic rules of both languages (Glues) which needs to put some strong restriction on how the Glue is mimicked.





